$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), $a$:$T$, $L$:($T$ List), $b$:$T$.
\\[0ex]($b$ $\in$ insert(${\it eq}$; $a$; $L$)) $\Leftarrow\!\Rightarrow$ (($b$ = $a$) $\vee$ ($b$ $\in$ $L$))